\begin{tabbing}
msg{-}item(${\it ds}$; ${\it da}$; $k$; $l$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=${\it tg}$:Id\+
\\[0ex]$\times$ ($n$:$\mathbb{N}$
\\[0ex]$\times$ (decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$(fpf{-}cap(${\it da}$; Kind{-}deq; rcv($l$,${\it tg}$); void) List)))
\-
\end{tabbing}